<?php
	class CharStreamState {
	}
?>